A:MsgA.
AtomFree(ds(A))
 AtomFree(da(A))
 AtomFree(Type;b:IdA.state(TopA.da(locl(b))Top+Top)) 

latex

Definitions	t  T, P  Q, x:A. B(x), Prop
Lemmas	msga wf, ma ds wf, id-deq wf, Id wf, ma da wf, Kind-deq wf, Knd wf, atom-free-decl wf, atom-free-ma-state, atom-free-Id, locl wf, atom-free-ma-da